k:FinProbSpace, n:, X:RandomVariable(k;n), q:. q*X  RandomVariable(k;n) 

latex

Definitions	t  T, , x:A. B(x), ||as||, P & Q, i  j < k, a < b, P  Q, False, A, A  B, , {x:A| B(x)} , {i..j}, #$n, Void, x:AB(x), l[i], x. t(x), a  j < b. E(j), s = t, type List, , Type, f(a), r * s, x.A(x), q*X, RandomVariable(p;n), FinProbSpace
Lemmas	qmul wf, nat wf, qsum wf, select wf, int seg wf, int inc rationals, length wf1, rationals wf